|
| 1: |
|
app'(app'(minus,x),0) |
→ x |
| 2: |
|
app'(app'(minus,app'(s,x)),app'(s,y)) |
→ app'(app'(minus,x),y) |
| 3: |
|
app'(app'(minus,app'(app'(minus,x),y)),z) |
→ app'(app'(minus,x),app'(app'(plus,y),z)) |
| 4: |
|
app'(app'(quot,0),app'(s,y)) |
→ 0 |
| 5: |
|
app'(app'(quot,app'(s,x)),app'(s,y)) |
→ app'(s,app'(app'(quot,app'(app'(minus,x),y)),app'(s,y))) |
| 6: |
|
app'(app'(plus,0),y) |
→ y |
| 7: |
|
app'(app'(plus,app'(s,x)),y) |
→ app'(s,app'(app'(plus,x),y)) |
| 8: |
|
app'(app'(app,nil),k) |
→ k |
| 9: |
|
app'(app'(app,l),nil) |
→ l |
| 10: |
|
app'(app'(app,app'(app'(cons,x),l)),k) |
→ app'(app'(cons,x),app'(app'(app,l),k)) |
| 11: |
|
app'(sum,app'(app'(cons,x),nil)) |
→ app'(app'(cons,x),nil) |
| 12: |
|
app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) |
→ app'(sum,app'(app'(cons,app'(app'(plus,x),y)),l)) |
| 13: |
|
app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) |
→ app'(sum,app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k))))) |
|
There are 24 dependency pairs:
|
| 14: |
|
APP'(app'(minus,app'(s,x)),app'(s,y)) |
→ APP'(app'(minus,x),y) |
| 15: |
|
APP'(app'(minus,app'(s,x)),app'(s,y)) |
→ APP'(minus,x) |
| 16: |
|
APP'(app'(minus,app'(app'(minus,x),y)),z) |
→ APP'(app'(minus,x),app'(app'(plus,y),z)) |
| 17: |
|
APP'(app'(minus,app'(app'(minus,x),y)),z) |
→ APP'(app'(plus,y),z) |
| 18: |
|
APP'(app'(minus,app'(app'(minus,x),y)),z) |
→ APP'(plus,y) |
| 19: |
|
APP'(app'(quot,app'(s,x)),app'(s,y)) |
→ APP'(s,app'(app'(quot,app'(app'(minus,x),y)),app'(s,y))) |
| 20: |
|
APP'(app'(quot,app'(s,x)),app'(s,y)) |
→ APP'(app'(quot,app'(app'(minus,x),y)),app'(s,y)) |
| 21: |
|
APP'(app'(quot,app'(s,x)),app'(s,y)) |
→ APP'(quot,app'(app'(minus,x),y)) |
| 22: |
|
APP'(app'(quot,app'(s,x)),app'(s,y)) |
→ APP'(app'(minus,x),y) |
| 23: |
|
APP'(app'(quot,app'(s,x)),app'(s,y)) |
→ APP'(minus,x) |
| 24: |
|
APP'(app'(plus,app'(s,x)),y) |
→ APP'(s,app'(app'(plus,x),y)) |
| 25: |
|
APP'(app'(plus,app'(s,x)),y) |
→ APP'(app'(plus,x),y) |
| 26: |
|
APP'(app'(plus,app'(s,x)),y) |
→ APP'(plus,x) |
| 27: |
|
APP'(app'(app,app'(app'(cons,x),l)),k) |
→ APP'(app'(cons,x),app'(app'(app,l),k)) |
| 28: |
|
APP'(app'(app,app'(app'(cons,x),l)),k) |
→ APP'(app'(app,l),k) |
| 29: |
|
APP'(app'(app,app'(app'(cons,x),l)),k) |
→ APP'(app,l) |
| 30: |
|
APP'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) |
→ APP'(sum,app'(app'(cons,app'(app'(plus,x),y)),l)) |
| 31: |
|
APP'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) |
→ APP'(app'(cons,app'(app'(plus,x),y)),l) |
| 32: |
|
APP'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) |
→ APP'(cons,app'(app'(plus,x),y)) |
| 33: |
|
APP'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) |
→ APP'(app'(plus,x),y) |
| 34: |
|
APP'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) |
→ APP'(plus,x) |
| 35: |
|
APP'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) |
→ APP'(sum,app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k))))) |
| 36: |
|
APP'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) |
→ APP'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k)))) |
| 37: |
|
APP'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) |
→ APP'(sum,app'(app'(cons,x),app'(app'(cons,y),k))) |
|
The approximated dependency graph contains one SCC:
{14,16,17,20,22,25,27,28,30,31,33,35-37}.